package main;

import java.util.HashMap;
import java.util.Map;
import java.util.Vector;

public class LiteralAlocatorAndMap {
	
	private Map<Integer,Pair<Integer, Integer>> litsToEdges;
	private Map< Integer, String> otherLitsWithDescription;
	private int litCounter;
	private int zeroLiteral;
	private int numOfVertices;
	private int[] sumBits;
	private HashMap<Pair<Integer, Integer>, Integer> edgesToLits;
	public LiteralAlocatorAndMap(int numOfVertices) {
		litsToEdges = new HashMap<Integer,Pair<Integer, Integer>>();
		edgesToLits = new HashMap<Pair<Integer, Integer>, Integer>();
		otherLitsWithDescription = new HashMap< Integer, String>();
		litCounter = 1;
		zeroLiteral = -1;
		this.numOfVertices = numOfVertices;
		sumBits = null;
	}
	
	public void setSumBits(int[] sumBits){
		this.sumBits = sumBits;
	}
	
	public int[] getSumBits(){
		return this.sumBits;
	}
	
	/**
	 * Precondition: first call generateMap
	 * @return
	 */
	public Map<Integer,Pair<Integer, Integer>> getLiteralsToEdgesMap(){
		return litsToEdges;
	}

	public int getNumOfEdgeLiteral(){
		return litsToEdges.size();
	}
	
	public int[] getEdgeLiterals(){
		int[] lits = new int[litsToEdges.size()/2];
		int cnt = 0;
		for (int lit : litsToEdges.keySet()){
			if (lit%2 == 1)
				lits[cnt++] = lit;
		}
		
		return lits;
	}
	
	public Vector<int[]> generateMap(){
		
		Vector<int[]> cnf = new Vector<int[]>();
		
		for (int i = 1; i<=numOfVertices; i++){
			for (int j = i+1; j<=numOfVertices; j++){
				int c1 = litCounter++;
				int c2 = litCounter++;
				Pair<Integer, Integer> pair = new Pair<Integer, Integer>(i, j);
				litsToEdges.put(c1, pair);
				edgesToLits.put(pair, c1);
				pair = new Pair<Integer, Integer>(j, i);
				litsToEdges.put(c2, pair);
				edgesToLits.put(pair,c2);
				
				cnf.add(new int[]{c1, -c2});
				cnf.add(new int[]{-c1, c2});
			}
		}
		
		return cnf;
	}
	
	public int newLiteral(String description){
		int newLit = litCounter++;
		otherLitsWithDescription.put(newLit, description);
		return newLit;
	}
	
	public int newLiteral(){
		return newLiteral("");
	}
	
	public int lastLiteral(){
		return litCounter-1;
	}

	public int getZeroLit(){
		if (zeroLiteral == -1){
			zeroLiteral = newLiteral("zero");
		}
		return zeroLiteral;
	}
	
	public int getNumOfVertices() {
		return numOfVertices;
	}

	public int[] getRowLits(int rowIndex){
		int[] res = new int[getNumOfVertices()];
		for (int i = rowIndex + 1; i<= getNumOfVertices(); i++){
			if (i != rowIndex){
				res[i-1] = edgesToLits.get(new Pair<Integer, Integer>(rowIndex, i));
			}else{
				res[i-1] = getZeroLit();
			}
		}
		return res;
	}

	public int getEdgeLiteral(Pair<Integer, Integer> edge) {
		
		return edgesToLits.get(edge);
	}
	
}
